Nuprl Lemma : qle_weakening_eq_qorder 11,40
a, b:. (a = b)  a  b 
latex

Definitionsx,y. t(x;y), , x f y, t  T, OMon, t.1, Mon, x(s1,s2), P & Q, AbMon, OCMon, OGrp, <+>, |g|, x:A. B(x), r  s
Lemmasocgrp wf, grp le wf, assert wf, grp car wf, linorder wf, qadd grp wf2, grp leq weakening eq

origin